Issue2790.agda:7,1-21
Could not generate equivalence when splitting on indexed family,
the function will not compute on transports by a path.
  Reason: WithKEnabled
when checking the definition of uip
Issue2790.agda:7,1-21
Could not generate equivalence when splitting on indexed family,
the function will not compute on transports by a path.
  Reason: WithKEnabled
when checking the definition of uip

———— All done; warnings encountered ————————————————————————

Issue2790.agda:7,1-21
Could not generate equivalence when splitting on indexed family,
the function will not compute on transports by a path.
  Reason: WithKEnabled
when checking the definition of uip

Issue2790.agda:7,1-21
Could not generate equivalence when splitting on indexed family,
the function will not compute on transports by a path.
  Reason: WithKEnabled
when checking the definition of uip
